|
The McCarthy 91 function is a recursive function, defined by the computer scientist John McCarthy as a test case for formal verification within computer science. The McCarthy 91 function is defined as : The results of evaluating the function are given by ''M''(''n'') = 91 for all integer arguments ''n'' ≤ 100, and ''M''(''n'') = ''n'' − 10 for ''n'' > 100. Indeed, the result of M(101) is also 91 (101 - 10 = 91). All results of M(n) after n = 101 are continually increasing by 1, e.g. M(102) = 92, M(103) = 93. ==History== The 91 function was introduced in papers published by Zohar Manna, Amir Pnueli and John McCarthy in 1970. These papers represented early developments towards the application of formal methods to program verification. The 91 function was chosen for having a complex recursion pattern (contrasted with simple patterns, such as defining by means of ). The example was popularized by Manna's book, ''Mathematical Theory of Computation'' (1974). As the field of Formal Methods advanced, this example appeared repeatedly in the research literature. In particular, it is viewed as a "challenge problem" for automated program verification. Often, it is easier to reason about non-recursive computation. As one of the examples used to demonstrate such reasoning, Manna's book includes a non-recursive algorithm that simulates the original (recursive) 91 function. Many of the papers that report an "automated verification" (or termination proof) of the 91 function only handle the non-recursive version. A formal derivation of the non-recursive version from the recursive one was given in a 1980 article by Mitchell Wand, based on the use of continuations. 抄文引用元・出典: フリー百科事典『 ウィキペディア（Wikipedia）』 ■ウィキペディアで「McCarthy 91 function」の詳細全文を読む スポンサード リンク
|